/*
 * Created on 2005/5/5
 *
 * TODO To change the template for this generated file go to
 * Window - Preferences - Java - Code Style - Code Templates
 */
package alloy.semantic;

import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;

import alloy.ast.ASTDepthFirstVisitor;
import alloy.ast.Decl;
import alloy.ast.Module;
import alloy.ast.ModuleInfo;
import alloy.ast.SigExpr;
import alloy.ast.Signature;
import alloy.type.SigType;
import alloy.util.Dbg;

/**
 * counts the number of times a signature is referenced in FIELD DECLARATIONS in the model. this is used for
 * an atomization heuristic.
 */
public class SignatureReferenceCounter extends ASTDepthFirstVisitor {

    public class CountTree {

        Map sigTypeToNode = new HashMap();

        public CountTreeNode addNode(CountTreeNode parent_, SigType type_) {
            CountTreeNode childNode = new CountTreeNode(type_);
            childNode.setParent(parent_);
            
            if (parent_ != null) {
                parent_.addChild(childNode);
            }
            sigTypeToNode.put(type_, childNode);

            return childNode;
        }

        public CountTreeNode getCountTreeNode(SigType type_) {
            return (CountTreeNode) sigTypeToNode.get(type_);
        }

        public void updateNode(SigType type_, int updateAmount) {
            CountTreeNode node = getCountTreeNode(type_);
            while (node != null) {
                node.addCount(updateAmount);
                node = node.getParent();
            }
        }

        public int getCount(SigType type_) {
            CountTreeNode node = getCountTreeNode(type_);
            if (node != null) {
                return node.getCount();
            }

            return -1;
        }
        
        public String toString() {
            StringBuffer buf = new StringBuffer();
            // print depth first
            
            
            for (Iterator valIter = sigTypeToNode.values().iterator(); valIter.hasNext(); ) {
                CountTreeNode node = (CountTreeNode) valIter.next();
                
                if (node.getParent() == null) {
                    toStringHelper(buf, node, 0);
                }
            }
                                    
            
            return buf.toString();
        }
        
        private void toStringHelper(StringBuffer buf, CountTreeNode node, int depth) {
            for (int i = 0; i< depth; i++) buf.append("  ");
            buf.append(node.toString()+"\n");
            
            Iterator children = node.getChildren(); 
            
            while (children.hasNext()) {
                toStringHelper(buf, (CountTreeNode) children.next(), depth+1);
            }
        }
    }

    public class CountTreeNode {

        private int _count;
        private SigType _type;

        private CountTreeNode _parent;
        private List _children;

        private CountTreeNode(SigType type_) {
            _count = 0;
            _type = type_;
            _children = new LinkedList();
        }

        public void addCount(int c_) {
            _count += c_;
        }

        public int getCount() {
            return _count;
        }

        public SigType getType() {
            return _type;
        }

        public void setParent(CountTreeNode parent_) {
            _parent = parent_;
        }
        public CountTreeNode getParent() {
            return _parent;
        }

        public boolean isRoot() {
            return _parent == null;
        }

        public void addChild(CountTreeNode c_) {
            _children.add(c_);
        }

        public Iterator getChildren() {
            return _children.iterator();
        }
        
        public String toString() {
            return _type.toShortString() + ": " + _count + "/ parent: " + (_parent == null ? "null" : _parent.getType().toShortString());
        }

    }

    private CountTree ct;
    private ModuleInfo moduleInfo;

    /**
     * Initializes the CountTree
     *  
     */
    public SignatureReferenceCounter() {
        ct = new CountTree();

        List rootTypes = new LinkedList();

        for (Iterator typesIter = SigType.getSigTypes().iterator(); typesIter.hasNext();) {
            SigType type = (SigType) typesIter.next();
            SigType superType = type.getSuperType();

            if (superType == null) {
                rootTypes.add(type);
            }
        }

        for (Iterator rootIter = rootTypes.iterator(); rootIter.hasNext();) {
            SigType root = (SigType) rootIter.next();

            CountTreeNode rootNode = ct.addNode(null, root);
            addChildren(rootNode, root);
        }
    }

    private void addChildren(CountTreeNode node, SigType type) {
        for (Iterator children = type.getSubTypes().iterator(); children.hasNext();) {
            SigType child = (SigType) children.next();

            CountTreeNode childNode = ct.addNode(node, child);
            addChildren(childNode, child);
        }
    }

    public void visit(Module module_) {        
        
        // if module does not contain any signatures,
        // do nothing
        if (!module_.getSignatures().getSignatureIter().hasNext())
            return;
        
        moduleInfo = module_.getModuleInfo();

        // visit signatures to look at field decls
        module_.getSignatures().applyVisitor(this);

        // set ModuleInfo's count tree to ct
        moduleInfo.setSigRefCountTree(ct);

    }

    public void visit(Signature signature_) {

        // visit the field declarations
        signature_.getDecls().applyVisitor(this);

    }

    public void visit(Decl decl_) {

        // visit the expression of the decl
        decl_.getExpr().applyVisitor(this);
    }

    public void visit(SigExpr sigExpr_) {

        SigType exprType = sigExpr_.getType().toRelationType().getSigType();
               
        Signature sig = moduleInfo.getSignature(sigExpr_.getSig(), null);
        
        if (sig == null) {
            return;
        }
        
        if (!sig.isSubset()) {
            // if refers to type, then increment
            // a bit wasteful to do +1 incrememnts since it's O(depth of tree), but this will
            // do for now.
            ct.updateNode(exprType, 1);
        }
    }

}